$\forall$$T$:Type, $n$:$\mathbb{N}$, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow$$T$), $i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$. ($f$\{$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$\})[$i$] $=$ $f$($i$)